Issue2332.agda:6,1-12
Cannot eliminate type  Set → Set₁  with projection  R._A
when checking that the clause P R.A = Set has type Set → Set₁
